import Yices hiding (gt, lt, xor)
import Data.Function

type Binary = Int -> Bool

-- Number of PCs
pcCount = 4
pcs = [0..pcCount-1]

decl :: (String -> a) -> String -> (a, a, a)
decl i n = (i n, i (n ++ "0"), i (n ++ "1"))

p', l', m' :: Ident (Int -> Bool)
((p',p),(p0',p0),(p1',p1)) = decl ident1 "p"
((l',l),(l0',l0),(l1',l1)) = decl ident1 "l"
((m',m),(m0',m0),(m1',m1)) = decl ident1 "m"

s',b' :: Ident (Int -> Binary)
((s',s),(s0',s0),(s1',s1)) = decl ident2 "s"
((b',b),(b0',b0),(b1',b1)) = decl ident2 "b"

-- Binary representation of a number
infix 4 .=
(.=) :: (Int -> Prop) -> Int -> Prop
x .= 0 = non (x 0) /\ non (x 1)
x .= 1 =      x 0  /\ non (x 1)
x .= 2 = non (x 0) /\      x 1
x .= 3 =      x 0  /\      x 1

gt :: (Int -> Prop) -> Int -> Prop
gt p 0 = p 0 \/ p 1
gt p 1 = p 1
gt p 2 = p 0 /\ p 1
gt p 3 = bool False

lt :: (Int -> Prop) -> Int -> Prop
lt p 0 = bool False
lt p 1 = non (p 0) /\ non (p 1)
lt p 2 = non (p 1)
lt p 3 = non (p 0) \/ non (p 1)

initial :: Prop
initial = conj [non (p i) /\ non (l i) /\ non (m i) | i <- pcs]

final :: Prop
final = disj
    [ taskA_inequalLeaders  /\ succFinish
    , taskB_leaderIsNotMax  /\ succFinish
    , taskC_deadlock        /\ non succFinish
    ]

-- Successful finish.
succFinish :: Prop
succFinish = disj [l i /\ m i /\ non (p i) | i <- pcs]

-- Not all leaders are equal.
taskA_inequalLeaders :: Prop
taskA_inequalLeaders = disj [ b i /= b j | i <- pcs, j <- pcs, i < j ]
  where
    x /= y = (x 0 `xor` y 0) \/ (x 1 `xor` y 1)
    xor x y = idt xor' ! x ! y

-- Leader hasn't got the maximal uid.
taskB_leaderIsNotMax :: Prop
taskB_leaderIsNotMax = disj [ non (b i .= (pcCount-1)) | i <- pcs ] 

-- A deadlock has occured.
taskC_deadlock :: Prop
taskC_deadlock = conj
    [  fails [non (p i), non (l i)]
    /\ fails [p i, non (l i), recv i (`gt` i)]
    /\ fails [p i, non (l i), recv i (.= i)]
    /\ fails [p i, l i]
    | i <- pcs
    ]
  where
    recv i p = m i /\ p (s i)
    fails    = non . conj

-- Transition: stop-the-world semantics for processor arrays.
trans :: Prop
trans = disj [tick i | i <- pcs]

-- Clock tick of a single processor.
tick :: Int -> Prop
tick i = conj [sleep k | k <- pcs, k /= i, k /= j] /\ pasv j /\ disj
    [ [non (p0 i), non (l0 i)]
        --> [p1 i, non (l1 i), b1 i == b0 i, norecv, send (.= i), pasvl j]
    , [p0 i, non (l0 i), recv (`gt` i)]
        --> [p1 i, non (l1 i), b1 i == b0 i, clrecv, send (== s0 i), pasvl j]
    , [p0 i, non (l0 i), recv (.= i)]
        --> [p1 i, l1 i, b1 i == b0 i, clrecv, nosend, pasvl j]
    , [p0 i, l0 i]
        --> [non (p1 i), l1 i, b1 i == s0 i, clrecv, send (== s0 i), l1 j]
    ]
  where
    j = (i+1) `mod` pcCount  -- next
    pasvl k = l1 k <-> l0 k
    pasv  k = (p1 k <-> p0 k) /\ (b1 k == b0 k)
    sleep k = pasv k /\ pasvl k /\ (m1 k <-> m0 k) /\ (s1 k == s0 k)
    recv p = m0 i /\ p (s0 i) -- receive a message
    send p = m1 j /\ p (s1 j) -- send a message to the next node
    nosend = (m1 j <-> m0 j) /\ (s1 j == s0 j) -- don't touch neighbor's mailbox
    norecv = (m1 i <-> m0 i) /\ (s1 i == s0 i) -- don't touch own mailbox
    clrecv = non (m1 i) /\ (s1 i == s0 i)
    xs --> ys = conj xs /\ conj ys
    x  <-> y  = iff' ! x ! y
    x   ==  y  = (x 0 <-> y 0) /\ (x 1 <-> y 1)

main = printBddReach initial trans final
